...в чем там проблема, но есть отличная книга "Верификация моделей программ". Там про разные варианты рассказывается.

Если я всё правильно помню (а книга запихнута довольно далеко), то можно поменять темпоральную логику и взять её вариант попроще. Соответственно, сложность упадёт.

К недавнему посту про ACL2.

Глава из книги "Computer-Aided Reasoning: ACL2 Case Studies."
http://www-static.cc.gatech.edu/fac/Pete.Manolios/research/acs-mu-calc.html

Abstract
Temporal logic model-checking has received substantial academic ( Read more... )